(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sb -> Sk *)

(* 侧滑角β (sidelip angle) *)
Parameter beta : R.

(* 迎角 α  (angle of attack) *)
Parameter alpha : R.

(* γ  *)
Parameter gamma : R.

Definition coordinate_transform_SaSk : Mat R 3 3 := mkMat_3_3
  1       0           0
  0 ( cos gamma) (sin gamma)
  0 (-sin gamma) (cos gamma).

Definition coordinate_transform_SbSa : Mat R 3 3 := mkMat_3_3
  ((cos alpha)*(cos beta))  (sin beta) ((sin alpha)*(cos beta))
  (-(cos alpha)*(sin beta)) (cos beta) (-(sin alpha)*(sin beta))
  (-sin alpha)                   0         (cos alpha).


Definition SbToSk : Mat R 3 3 := mkMat_3_3
((cos alpha)*(cos beta)) (sin beta) ((sin alpha)*(cos beta))
(-(cos gamma)*(cos alpha)*(sin beta)-(sin gamma)*(sin alpha)) ((cos gamma)*(cos beta)) (-(cos gamma)*(sin alpha)*(sin beta)+(sin gamma)*(cos alpha))
((sin gamma)*(cos alpha)*(sin beta)-(cos gamma)*(sin alpha)) (-(sin gamma)*(cos beta)) ((sin gamma)*(sin alpha)*(sin beta)+(cos gamma)*(cos alpha)).


Lemma SbToSk_eq:
  SbToSk === RMmul coordinate_transform_SaSk coordinate_transform_SbSa.
Proof.
  unfold SbToSk. RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. ring. f_equal3. ring. f_equal. ring. f_equal3. ring.
Qed.

